KILLED



    


Runtime Complexity (innermost) proof of /tmp/tmpqVbzDi/sum_sqs3.xml









The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, INF).

0 CpxTRS


↳1 RenamingProof (⇔, 0 ms)


↳2 CpxRelTRS


↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


↳4 typed CpxTrs


↳5 OrderProof (LOWER BOUND(ID), 0 ms)


↳6 typed CpxTrs


↳7 RewriteLemmaProof (LOWER BOUND(ID), 754 ms)


↳8 BEST


    ↳9 typed CpxTrs


        ↳10 RewriteLemmaProof (LOWER BOUND(ID), 3 ms)


        ↳11 BEST


            ↳12 typed CpxTrs


                ↳13 RewriteLemmaProof (LOWER BOUND(ID), 346 ms)


                ↳14 BEST


                    ↳15 typed CpxTrs


                        ↳16 RewriteLemmaProof (LOWER BOUND(ID), 83 ms)


                        ↳17 BEST


                            ↳18 typed CpxTrs


                            ↳19 typed CpxTrs


                    ↳20 typed CpxTrs


            ↳21 typed CpxTrs


    ↳22 typed CpxTrs









(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:

sum#1(Nil) → 0

sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))

map#2(Nil) → Nil

map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))

unfoldr#2(0) → Nil

unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))

mult#2(0, x2) → 0

mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))

plus#2(0, x8) → x8

plus#2(S(x4), x2) → S(plus#2(x4, x2))

main(0) → 0

main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Rewrite Strategy: INNERMOST




(1) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

sum#1(Nil) → 0'

sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))

map#2(Nil) → Nil

map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))

unfoldr#2(0') → Nil

unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))

mult#2(0', x2) → 0'

mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))

plus#2(0', x8) → x8

plus#2(S(x4), x2) → S(plus#2(x4, x2))

main(0') → 0'

main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

S is empty.
Rewrite Strategy: INNERMOST




(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(4) Obligation:
Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons




(5) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
sum#1, plus#2, map#2, mult#2, unfoldr#2
They will be analysed ascendingly in the following order:
plus#2 < sum#1
plus#2 < mult#2
mult#2 < map#2




(6) Obligation:
Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons
Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))
The following defined symbols remain to be analysed:
plus#2, sum#1, map#2, mult#2, unfoldr#2
They will be analysed ascendingly in the following order:
plus#2 < sum#1
plus#2 < mult#2
mult#2 < map#2




(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
Induction Base:
plus#2(gen_0':S3_0(0), gen_0':S3_0(b)) →RΩ(1)
gen_0':S3_0(b)
Induction Step:
plus#2(gen_0':S3_0(+(n6_0, 1)), gen_0':S3_0(b)) →RΩ(1)
S(plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b))) →IH
S(gen_0':S3_0(+(b, c7_0)))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).




(8) Complex Obligation (BEST)




(9) Obligation:
Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons
Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))
The following defined symbols remain to be analysed:
sum#1, map#2, mult#2, unfoldr#2
They will be analysed ascendingly in the following order:
mult#2 < map#2




(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n7310)
Induction Base:
sum#1(gen_Nil:Cons4_0(0)) →RΩ(1)
0'
Induction Step:
sum#1(gen_Nil:Cons4_0(+(n731_0, 1))) →RΩ(1)
plus#2(0', sum#1(gen_Nil:Cons4_0(n731_0))) →IH
plus#2(0', gen_0':S3_0(0)) →LΩ(1)
gen_0':S3_0(+(0, 0))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).




(11) Complex Obligation (BEST)




(12) Obligation:
Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons
Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n7310)
Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))
The following defined symbols remain to be analysed:
mult#2, map#2, unfoldr#2
They will be analysed ascendingly in the following order:
mult#2 < map#2




(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b)) → gen_0':S3_0(*(n1062_0, b)), rt ∈ Ω(1 + b·n10620 + n10620)
Induction Base:
mult#2(gen_0':S3_0(0), gen_0':S3_0(b)) →RΩ(1)
0'
Induction Step:
mult#2(gen_0':S3_0(+(n1062_0, 1)), gen_0':S3_0(b)) →RΩ(1)
plus#2(gen_0':S3_0(b), mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b))) →IH
plus#2(gen_0':S3_0(b), gen_0':S3_0(*(c1063_0, b))) →LΩ(1 + b)
gen_0':S3_0(+(b, *(n1062_0, b)))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).




(14) Complex Obligation (BEST)




(15) Obligation:
Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons
Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n7310)
mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b)) → gen_0':S3_0(*(n1062_0, b)), rt ∈ Ω(1 + b·n10620 + n10620)
Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))
The following defined symbols remain to be analysed:
map#2, unfoldr#2




(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
map#2(gen_Nil:Cons4_0(n2038_0)) → gen_Nil:Cons4_0(n2038_0), rt ∈ Ω(1 + n20380)
Induction Base:
map#2(gen_Nil:Cons4_0(0)) →RΩ(1)
Nil
Induction Step:
map#2(gen_Nil:Cons4_0(+(n2038_0, 1))) →RΩ(1)
Cons(mult#2(0', 0'), map#2(gen_Nil:Cons4_0(n2038_0))) →LΩ(1)
Cons(gen_0':S3_0(*(0, 0)), map#2(gen_Nil:Cons4_0(n2038_0))) →IH
Cons(gen_0':S3_0(0), gen_Nil:Cons4_0(c2039_0))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).




(17) Complex Obligation (BEST)




(18) Obligation:
Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons
Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n7310)
mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b)) → gen_0':S3_0(*(n1062_0, b)), rt ∈ Ω(1 + b·n10620 + n10620)
map#2(gen_Nil:Cons4_0(n2038_0)) → gen_Nil:Cons4_0(n2038_0), rt ∈ Ω(1 + n20380)
Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))
The following defined symbols remain to be analysed:
unfoldr#2




(19) Obligation:
Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons
Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n7310)
mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b)) → gen_0':S3_0(*(n1062_0, b)), rt ∈ Ω(1 + b·n10620 + n10620)
map#2(gen_Nil:Cons4_0(n2038_0)) → gen_Nil:Cons4_0(n2038_0), rt ∈ Ω(1 + n20380)
Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))
No more defined symbols left to analyse.




(20) Obligation:
Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons
Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n7310)
mult#2(gen_0':S3_0(n1062_0), gen_0':S3_0(b)) → gen_0':S3_0(*(n1062_0, b)), rt ∈ Ω(1 + b·n10620 + n10620)
Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))
No more defined symbols left to analyse.




(21) Obligation:
Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons
Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
sum#1(gen_Nil:Cons4_0(n731_0)) → gen_0':S3_0(0), rt ∈ Ω(1 + n7310)
Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))
No more defined symbols left to analyse.




(22) Obligation:
Innermost TRS:
Rules:
sum#1(Nil) → 0'
sum#1(Cons(x2, x1)) → plus#2(x2, sum#1(x1))
map#2(Nil) → Nil
map#2(Cons(x2, x5)) → Cons(mult#2(x2, x2), map#2(x5))
unfoldr#2(0') → Nil
unfoldr#2(S(x2)) → Cons(x2, unfoldr#2(x2))
mult#2(0', x2) → 0'
mult#2(S(x4), x2) → plus#2(x2, mult#2(x4, x2))
plus#2(0', x8) → x8
plus#2(S(x4), x2) → S(plus#2(x4, x2))
main(0') → 0'
main(S(x1)) → sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1)))))

Types:
sum#1 :: Nil:Cons → 0':S
Nil :: Nil:Cons
0' :: 0':S
Cons :: 0':S → Nil:Cons → Nil:Cons
plus#2 :: 0':S → 0':S → 0':S
map#2 :: Nil:Cons → Nil:Cons
mult#2 :: 0':S → 0':S → 0':S
unfoldr#2 :: 0':S → Nil:Cons
S :: 0':S → 0':S
main :: 0':S → 0':S
hole_0':S1_0 :: 0':S
hole_Nil:Cons2_0 :: Nil:Cons
gen_0':S3_0 :: Nat → 0':S
gen_Nil:Cons4_0 :: Nat → Nil:Cons
Lemmas:
plus#2(gen_0':S3_0(n6_0), gen_0':S3_0(b)) → gen_0':S3_0(+(n6_0, b)), rt ∈ Ω(1 + n60)
Generator Equations:
gen_0':S3_0(0) ⇔ 0'
gen_0':S3_0(+(x, 1)) ⇔ S(gen_0':S3_0(x))
gen_Nil:Cons4_0(0) ⇔ Nil
gen_Nil:Cons4_0(+(x, 1)) ⇔ Cons(0', gen_Nil:Cons4_0(x))
No more defined symbols left to analyse.